Predicate intuitionistic logic is a well established fragment of dependenttypes. According to the Curry-Howard isomorphism proof construction in thelogic corresponds well to synthesis of a program the type of which is a givenformula. We present a model of automata that can handle proof construction infull intuitionistic first-order logic. The automata are constructed in such away that any successful run corresponds directly to a normal proof in thelogic. This makes it possible to discuss formal languages of proofs orprograms, the closure properties of the automata and their connections with thetraditional logical connectives.
展开▼
